FDL - Step of Proof: neg_mul_arg_bounds

Step of Proof: neg_mul_arg_bounds

Inference at * 1 1 0
Iof proof for Lemma neg mul arg bounds:

1. a :

2. b :

3. ((-(a * b)) > (-0))

((((-a) > (-0)) & (b > 0))

(((-a) < (-0)) & (b < 0)))

((a * b) < 0)

(((a < 0) & (b > 0))

((a > 0) & (b < 0)))

by PERMUTE{1:n,

by PERMUTE{2:n,

by PERMUTE{3:n,

by PERMUTE{4:n,

by PERMUTE{5:n,

by PERMUTE{6:n,

by PERMUTE{7:n,

by PERMUTE{8:n,

by PERMUTE{9:n,

by PERMUTE{10:n,

by PERMUTE{11:n,

by PERMUTE{12:n,

by PERMUTE{13:n,

by PERMUTE{13:n,

by PERMUTE{5:n,

by PERMUTE{14:n,

by PERMUTE{15:n,

by PERMUTE{16:n,

by PERMUTE{17:n,

by PERMUTE{18:n,

by PERMUTE{18:n,

by PERMUTE{14:n,

by PERMUTE{5:n,

by PERMUTE{19:n,

by PERMUTE{20:n}

1: .....wf..... NILNIL

1:

((-(a * b)) > (-0))

2: .....wf..... NILNIL

2:

(0 > (a * b))

3: .....wf..... NILNIL

3:

((((-a) > (-0)) & (b > 0))

(((-a) < (-0)) & (b < 0)))

4: .....wf..... NILNIL

4:

(((0 > a) & (b > 0))

((a > 0) & (b < 0)))

5: .....wf..... NILNIL

5:

0

6: .....wf..... NILNIL

6:

(a * b)

7: .....wf..... NILNIL

7:

(((-a) > (-0)) & (b > 0))

8: .....wf..... NILNIL

8:

((0 > a) & (b > 0))

9: .....wf..... NILNIL

9:

(((-a) < (-0)) & (b < 0))

10: .....wf..... NILNIL

10:

((a > 0) & (b < 0))

11: .....wf..... NILNIL

11:

((-a) > (-0))

12: .....wf..... NILNIL

12:

(0 > a)

13: .....wf..... NILNIL

13:

(b > 0)

14: .....wf..... NILNIL

14:

a

15: .....wf..... NILNIL

15:

(b > 0) = (b > 0)

16: .....wf..... NILNIL

16:

((-a) < (-0))

17: .....wf..... NILNIL

17:

(a > 0)

18: .....wf..... NILNIL

18:

(b < 0)

19: .....wf..... NILNIL

19:

(b < 0) = (b < 0)

20:

20: 3. (0 > (a * b))

(((0 > a) & (b > 0))

((a > 0) & (b < 0)))

20:

((a * b) < 0)

(((a < 0) & (b > 0))

((a > 0) & (b < 0)))

.

Definitions t T, Type, x:A B(x), f(a), s = t, x:AB(x), , a < b, P Q, #$n, n * m, -n, , x:A. B(x), P Q, P Q, P & Q, i > j, P Q

Lemmas and functionality wrt iff, or functionality wrt iff, minus mono wrt lt, iff functionality wrt iff